\begin{tabbing}
$\forall$$i$, $x$:Id, $a$:Knd, $T$, $A$:Type, $f$:($A$$\rightarrow$$T$$\rightarrow$$A$).
\\[0ex]@$i$: ma{-}single{-}effect0($x$;$A$;$a$;$T$;$f$) $\in$ Dsys
\\[0ex]\& (\=$\forall$$D$:Dsys.\+
\\[0ex]@$i$: ma{-}single{-}effect0($x$;$A$;$a$;$T$;$f$) $\subseteq$ $D$
\\[0ex]$\Rightarrow$ \=$D$ \+
\\[0ex]realizes ${\it es}$.
\\[0ex]vartype($i$;$x$) $\subseteq\rho$ $A$ \& ($\forall$$e$:E. loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ kind($e$) $=$ $a$ $\in$ Knd $\Rightarrow$ valtype($e$) $\subseteq\rho$ $T$)
\\[0ex]\& (\=$\forall$$e$:E.\+
\\[0ex]loc($e$) $=$ $i$ $\in$ Id $\Rightarrow$ kind($e$) $=$ $a$ $\in$ Knd $\Rightarrow$ ($x$ after $e$) $=$ $f$(($x$ when $e$),val($e$)) $\in$ $A$))
\-\-\-
\end{tabbing}